The present invention is generally related to the field of software development and in particular describes techniques for the formal analysis and verification of software.
Model checking is a technique used for the automatic verification of concurrent software systems. It exhibits numerous advantages over other techniques such as simulation, testing, and deductive reasoning, and has been used successfully in practice to verify complex sequential circuit designs and communication protocols. (See E. M. Clarke, O. Grumberg, and D. A. Peled, “Model Checking,” MIT Press, 2000.) Of particular advantage, model checking is an automatic technique, and if a design being tested contains an error, the model checking technique produces a counter-example (i.e., a witness of the offending behavior of the system) that can be used to debug the system.
An alternative technique for the verification of software systems—symbolic model checking using binary decision diagrams (BDDs)—potentially provides exhaustive coverage of large state-spaces. Unfortunately, symbolic model checking using BDDs does not scale well in practice.
Yet another alternative technique for the verification of software systems is bounded model checking (BMC) focusing on the search for counter-examples of bounded length only. See, for example, A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” Proc. of the 36th ACM/IEEE Design Automation Conference, pp. 317-20 (1999). This technique effectively translates a problem to a Boolean formula, such that the formula is satisfiable if and only if there exists a counter-example of length k. In practice, k can be increased incrementally starting from one to find a shortest counter-example—if one exists. However, additional reasoning is needed to ensure completeness of the verification when no counter-example exists.
The satisfiability check in the BMC technique is typically performed by what is generally known as a “back-end” SAT-solver. See, e.g., M. K. Ganai, L. Zhang, P. Ashar, and A. Gupta, “Combining strength of circuit-based and CNF-based algorithms for a high performance SAT solver,” in Design Automation Conference, 2002; E. Goldberg and Y. Novikov, “Berkmin: A fast and robust SAT solver,” in Design Automation and Test in Europe, pages 132-39, 2002; J. P. Marques-Silva and K. A. Sakallah, “GRASP: A search algorithm for prepositional satisfiability,” IEEE Transactions on Computers, 48:506-2 1, 1999; and M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an efficient SAT solver in Design Automation Conference, 2001.
Recently, it has been proposed to apply bounded model checking techniques to the formal verification of software using predicate abstraction in a counterexample-guided refinement flow. See co-pending commonly-assigned Non-Provisional Utility Patent Application Ser. No. 11/040,409, entitled “SYSTEM AND METHOD FOR MODELING, ABSTRACTION, AND ANALYSIS OF SOFTWARE,” filed on Jan. 21, 2005, the contents of which are incorporated by reference herein. It would be advantageous to improve the performance of the abstraction refinement loop used in such verification tools. Moreover, it would be particularly advantageous to avoid computationally expensive ways of discovering new predicates such as interpolation.